Nuprl Lemma : random_wf
0,22
postcript
pdf
i
,
j
:
.
i
j
random(
i
;
j
)
{
i
..(
j
+1)
}
latex
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
,
A
B
,
#$n
,
n
+
m
,
a
<
b
,
x
:
A
B
(
x
)
,
P
&
Q
,
i
j
<
k
,
P
Q
,
False
,
A
,
Void
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
) }
,
{
i
..
j
}
,
random(
i
;
j
)
Lemmas
le
wf
origin
i, j:
. i
j 
random(i;j) 
{i..(j+1)
} i, j:. ij random(i;j) {i..(j+1)} Tx:A. B(x)B
B(x) j < k Q
A
B(x)}